COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Just as ZM and WP were telling me, my minimal fixed point schema is
C00007 00003	∂28-Jan-77  2035	WP   
C00011 00004	∂03-Feb-77  2045	WP   
C00013 ENDMK
C⊗;
Just as ZM and WP were telling me, my minimal fixed point schema is
related to subgoal induction.  Namely, it is a subcase of subgoal
induction, and subgoal induction also takes the form of an axiom schema.
This note is a reaction to WP's 1/26 handwritten note.

	Suppose, as in that note, we have the recursive definition

	f(x) ← if t x then  h x else g1 f g2 x.

This gives rise to the first order logic formula

	∀x.(f x = if t x then h x else g1 f g2 x)

and the minimal fixed point schema

	∀x.(indomain(if t x then h x else g1 g g2 x) ⊃
		g x = if t x then h x else g1 g g2 x)
	⊃ ∀x.(indomain(f(x)) ⊃ f(x) = g(x)).

(I hope omitting parentheses somewhat inconsistently after one argument
functions and predicates hasn't caused confusion.)

	However, the general rule of subgoal induction for this function
can also be expressed as an axiom schema, namely

∀x.(t x ⊃ q(x,h x)) ∧
∀x z.(¬t(x) ∧ q(g2 x,z) ⊃ q(x,g1 z)) ∧
∀x.(P(x) ∧ q(x,z) ⊃ Q(x,z))
⊃
∀x.(P(x) ∧ indomain(f(x)) ⊃ Q(x,f(x)))

where q, P, and Q are considered free predicate variables of the appropriate
numbers of arguments.

	Now the minimal fixed point schema is an instance of the
subgoal induction schema - namely we take

q(x,y) to be y = g(x)
P(x) to be always true
Q(x,y) to be y = g(x).

	This seems to be a simpler proof of the main result of WP's note.

	Notice that the Cartwright idea of saying indomain(x) for saying
that x is defined is required in order to express subgoal induction
as an axiom schema in logic.  This suggests that other methods of proving
partial correctness can also be described as axiom schemata.

	In fact consider the mutually recursive definitions

	f1 x ← if p1 x then x else f2 h1 x

	f2 x ← if p2 x then x else f1 h2 x

which give rise to the axioms

	∀x.(f1 x = if p1 x then x else f2 h1 x)

and

	∀x.(f2 x = if p2 x then x else f1 h2 x),

and a minimization schema involving two function variables which I won't
write down.

	The inductive assertion method is then expressed by the schema

	∀x.(P(x) ⊃ q1(x,x)) ∧
	∀x u.(q1(x,u) ⊃ if p1 u then Q(x,u) else q2(x,h1 u)) ∧
	∀x u.(q2(x,u) ⊃ if p2 u then Q(x,u) else q1(x,h2 u)) ∧
	⊃
	∀x.[P(x) ∧ indomain(f1(x)) ⊃ Q(x,f1(x))]

where P, q1, q2 and Q are all predicate variables taking the indicated
numbers of arguments.  The fact that indomain occurs only once in the
schema and not at all in the equations may seem odd, but it must occur
in some induction schema in the axiomatization of the basic functions
and predicates p1, p2, h1 and h2 or you won't be able to prove anything
non-trivial.

Questions:

	1. What other valid schemata are there?

	2. How do we express the inductive assertion method as a single
higher order schema independent of the number of functions being mutually
defined and with the specific recursion schemes expressed by instantiating
higher order function parameters?

∂28-Jan-77  2035	WP   
To:   JMC, ZM, WP 

This is an addition to John's two notes and my handwritten remark.
 
Suppose g satifies the fixed point axiom schema and we can prove a
program correct with respect to P and Q using the subgoal assertion q,
I will show that we can also prove the correctness with respect to
P and Q using the subgoal assertion g(x)=y ( we saw that this is in 
fact a subgoal assertion). This means that the subgoal assertion g(x)=y
is the strongest assertion possible.

 
I will assume that g(x)=y means indomain(y), hence indomain(g x).
 
I'll prove the following lemma:
 
indomain(f x) ∧ g(x)=y ⊃ q(x,y) 
for any g satisfying
	∀x.(indomain(if t x then h x else g1 g g2 x) ⊃
		g x = if t x then h x else g1 g g2 x)
and any arbitrary q satisfying
	∀x.(t x ⊃ q(x,h x)) ∧
	∀x z.(¬t(x) ∧ q(g2 x,z) ⊃ q(x,g1 z))
 
 
Proof:
By cases:
1. tx: this implies g(x)=h(x) as well as q(x,hx), since g is a function
	hx is the only y such that gx=y and we have q(x,y).
2. ¬tx:	We will prove this by contradiction. We assume ¬q(x,gx).
	Since q satifes the VC's we have q(g2 x, z) ⊃ q(x,g1 z) or
(*) 	¬q(x,g1 z) ⊃ ¬q(g2 x,z). 
	indomain(f x) ∧ ¬t x → indomain(f g2 x) → indomain(g g2 x) →
	g x = g1 g g2 x. Our assumption now becomes ¬q(x,g1 g g2 x),
	substituting in (*) we get ¬q(x,gx) ⊃ ¬(g2 x, g g2 x).
	This requires t(g2 x), because otherwise we get a contradiction
	with case 1. Assuming ¬t(g2 x), we can apply the same reasoning
	and finally get:
	∀n.g2↑n(x)=z ⊃ ¬q(z,gz) and  ∀n.¬t(g2↑n(x)). The latter
	implies that f is not defined for x, i.e. will not terminate,
	which gives the contradiction to indomain(f x).
						q.e.d.
 
Application of the lemma:
If we use q to prove a program correct with respect to P and Q, i.e.
we show P(x) ∧ q(x,y) ⊃ Q(x,y), then we set P'(x) ≡ P(x) ∧ indomain(fx).
We now have :
P'(x) ∧ g(x)=y ⊃ P(x) ∧ q(x,y) ⊃ Q(x,y) hence we have
P'(x) ∧ g(x)=y ⊃ Q(x,y) , i.e. g(x)=y proves our program correct
with respect to P' and Q. (Note that the other VC's are satisfied for
g(x)=y according to previous notes.) We cannot expect more, because for 
nonterminating x we can prove arbitrary nonsense, so it is not reasonable
to require the same things to be proved with the other assertion.
 
Together with the previous notes we have the result that the use
of the fol axiom schema is a special case of subgoal induction, but 
on the other hand it allows to prove the strongest results possible.

∂03-Feb-77  2045	WP   
To:   JMC, WP
Prove of the subgoal induction axiom schema.
 
We suppose the fixed point schema is valid, i.e.

	∀x.(indomain(if t x then h x else g1 g g2 x) ⊃
		g x = if t x then h x else g1 g g2 x)
	⊃ ∀x.(indomain(f(x)) ⊃ f(x) = g(x)).

We prove the validity of the subgoal induction schema:

∀x.(t x ⊃ q(x,h x)) ∧
∀x z.(¬t(x) ∧ q(g2 x,z) ⊃ q(x,g1 z)) ∧
∀x.(P(x) ∧ q(x,z) ⊃ Q(x,z))
⊃
∀x.(P(x) ∧ indomain(f(x)) ⊃ Q(x,f(x)))
 
Using the lemma proved in my previous note, i.e.

	indomain(f x) ∧ g(x)=y ⊃ q(x,y) 
	  for any g satisfying
	∀x.(indomain(if t x then h x else g1 g g2 x) ⊃
		g x = if t x then h x else g1 g g2 x)
	  and any arbitrary q satisfying
	∀x.(t x ⊃ q(x,h x)) ∧
	∀x z.(¬t(x) ∧ q(g2 x,z) ⊃ q(x,g1 z))
 
Since g satisfies the fixed point schema we have 
	indomain(fx) ⊃ fx = gx, and we can rewrite the lemma
	indomain(fx) ⊃ q(x, fx).
 
Together with P(x) ∧ q(x,z) ⊃  Q(x,z) we have
 
P(x) ∧ indomain(fx) ⊃ P(x) ∧ q(x,fx) ⊃ Q(x,fx).
 
hence ∀x.(P(x) ∧ indomain(f(x)) ⊃ Q(x,f(x))).
 
						q.e.d.
 
 
 
I'm still working on the relation to inductive assertions,
Wolf.